Add subsequence and slice split operations#164
Conversation
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: da13578af9
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| #[allow(dead_code)] | ||
| #[thrust::def::seq_subsequence] | ||
| #[thrust::ignored] | ||
| pub fn subsequence<U, V>(self, _start: U, _end: V) -> Self |
There was a problem hiding this comment.
When compiling any of the new split specs that call slice.subsequence(...) or (*slice).subsequence(...), this by-value receiver tries to move the Seq out of a shared reference or Mut deref in the generated formula function. Since Seq is not Copy, those extern specs fail type checking before verification; make this helper take &self (as len does) or otherwise avoid moving the receiver.
Useful? React with 👍 / 👎.
| thrust_models::model::Mut::new((*slice)[0], (!slice)[0]), | ||
| thrust_models::model::Mut::new( | ||
| (*slice).subsequence(1, (*slice).length), | ||
| (!slice).subsequence(1, (!slice).length), | ||
| ), |
There was a problem hiding this comment.
When a caller writes through a reference returned by split_first_mut or split_last_mut, this contract only nests the returned futures inside the tuple and never reassembles !slice from them the way first_mut/index_mut do. The current prophecy/drop handling does not propagate mutable updates out of tuple fields, so the added mutation fail test can mutate first and still prove a false fact about slice[0]; until !slice is explicitly tied to the returned refs, these split-mut specs are unsound.
Useful? React with 👍 / 👎.
coord-e
force-pushed
the
claude/seq-offset-field
branch
from
aa50d26 to
0c6bb28
Compare
`Seq::subsequence(start, end)` produces a view over the same underlying array with the offset advanced by `start` and the length set to `end - start`. It is used to describe the tail/init views returned by the slice split operations. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi
Both return the boundary element together with a subsequence view of the rest: `split_first` pairs `&slice[0]` with `slice[1..]`, and `split_last` pairs `&slice[len - 1]` with `slice[..len - 1]`. Paired pass/fail tests cover the returned element and the length and contents of the remaining view. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi
Both hand back a mutable reference to the boundary element together with a mutable subsequence view of the rest, mirroring the immutable split specs. Read-only pass/fail tests cover the returned element and the remaining view. A mutation through the first reference is not yet propagated back to the original slice when the reference is returned inside a tuple, which is unsound; `slice_split_first_mut_mutation_unsound` reproduces this and is expected to keep failing until the fix lands on main. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi
coord-e
force-pushed
the
claude/seq-subsequence-splits
branch
from
da13578 to
218028d
Compare
2 participants
Summary
PR 4 of 4 restructuring #153. Stacked on top of #163. Contains three commits:
Seq::subsequence(start, end)— a view over the same underlying array with the offset advanced bystartand the length set toend - start. Used to describe the tail/init views of the split operations (no dedicated test — it is exercised through the split tests).split_first/split_last— return the boundary element together with a subsequence view of the rest, with paired pass/fail tests.split_first_mut/split_last_mut— the mutable counterparts, with read-only pass/fail tests.Known limitation (expected CI failure)
A mutation through a
&mutreturned inside a tuple (assplit_first_mutdoes) is not yet propagated back to the original slice, which is unsound.tests/ui/fail/slice_split_first_mut_mutation_unsound.rsreproduces this and is expected to keep failing until the fix lands onmain— it is intentionally left as-is here. See the discussion on #124: #124 (comment)Validation
cargo build,cargo fmt --all -- --check,cargo clippy -- -D warningscargo test— all newsplit_first/split_last(_mut) pass/fail tests pass under the default Spacer solver; the only unexpected-looking failure is the intentional unsoundness reproduction above. (PCSat-backed tests require the CoAR Docker image and were not run here.)Stack
concat_int_arraytakes sequence tuples (Make concat_int_array operate on sequence tuples #162)split_first/split_last(_mut)🤖 Generated with Claude Code
https://claude.ai/code/session_01GzapTuen2mKHkkN3B7d8qi
Generated by Claude Code